Lean 语言参考手册

5. 源文件与模块🔗

在 Lean 中，编译的最小单位是单个 源文件。 源文件可以按文件名导入其它源文件。 换句话说，文件的名称和文件夹结构在 Lean 代码中具有重要意义。

每个源文件都有一个 导入名。它由文件名和 Lean 的启动方式共同决定：Lean 会在一组根目录中查找代码；源文件的导入名由从根目录到该文件的各级目录名和文件名组成，以点（.）分隔，并去掉 .lean 后缀。 例如，如果 Lean 以 Projects/MyLib/src 作为根目录，那么文件 Projects/MyLib/src/Literature/Novel/SciFi.lean 可用 Literature.Novel.SciFi 导入。

5.1. 编码与表示🔗

Lean 源文件是采用 UTF-8 编码的 Unicode 文本文件。 文件的每一行可以以换行字符（\n，Unicode 'LINE FEED (LF)' (U+000A)）结尾，也可以以回车加换行序列（\r\n，即 Unicode 'CARRIAGE RETURN (CR)' (U+000D) 加 'LINE FEED (LF)' (U+000A)）结尾。 不过，在解析或比较文件时，Lean 会对行尾进行归一化，因此所有文件在比较时都视为全部是 \n 行尾。

5.2. 具体语法🔗

Lean 的具体语法是 可扩展的。 在 Lean 这样的语言中，无法一次性完整地描述所有语法，因为库中还可以定义新的语法、常量，或者 归纳类型。 本节不会详尽描述整个语言，而是介绍整体框架；各个语言结构的具体语法则在其各自章节中详细说明。

5.2.1. 空白符🔗

Lean 中的词法单元（token）之间可以用任意数量的 空白符 字符序列分隔。 空白符可以是空格 (" ", Unicode 'SPACE (SP)' (U+0020))、合法的换行序列，或注释。 制表符和单独的回车（CR，未跟随换行）不是合法的空白符序列。

5.2.2. 注释🔗

注释是文件中虽然不是空白符，但被视为空白的部分。 Lean 提供两种注释语法：

行注释

当 -- 不作为其他词法单元一部分出现时，表示行注释。该标记后的所有内容直到行尾都会被视为空白字符。

块注释

当 /- 不作为其他词法单元一部分，且后面不是 - 字符时，表示块注释的开始。 块注释会一直持续到出现 -/ 终止为止。 块注释允许嵌套；仅在所有内部嵌套的 /- 都被匹配的 -/ 终止后，最外层才算结束。

/-- 与 /-! 用于开始 文档注释 ，它们同样以 -/ 结束，并允许嵌套块注释。 尽管文档注释看起来与普通注释类似，但在语法上它们属于不同类别；它们能出现的位置由 Lean 的语法决定。

5.2.3. 关键字与标识符🔗

一个 标识符 由一个或多个标识符成分（component）组成，各部分用 '.' 分隔。

标识符成分 由一个字母或类字母字符或下划线（'_'）开头，后面可以跟零个或多个标识符后续字符。 字母包括英文大小写字母，而类字母字符还包含范围较广的非英语字母脚本，包括 Lean 中广泛采用的希腊字母、科普特字母、Unicode 类字母符号区块（其中包含 ℕ、ℤ 等双线体字符和缩写）、Latin-1 补充字母（× 和 ÷ 除外），以及拉丁字母扩展 A 区块。 标识符的后续字符包括字母、类字母字符、下划线（'_'）、感叹号（!）、问号（?）、下标和单引号（'）。 作为例外，单独下划线不是合法的标识符。

标识符成分也可以用一对双 尖引号（'«' 和 '»'）括起来。 这样括起来的成分可以包含除 '»' 之外的任意字符，包括 '«'、. 和换行符。 尖引号本身不计入标识符最终内容，所以 «x» 和 x 是同一个标识符。 而 «Nat.add» 是一个包含一个成分的标识符，而 Nat.add 则包含两个成分。

可能的标识符成分中有一些属于保留关键字。 具体的保留关键字集合取决于当前激活的语法扩展集合，后者又依赖于已导入的模块以及当前打开的 命名空间；因此无法为整个 Lean 语言列举一个完整集合。 在大多数语法环境中，若要用关键字作为标识符成分，必须用尖引号括起来。 在某些环境下（如归纳类型的构造子名称）关键字无需尖引号也能作为标识符使用，这些环境称为 原始标识符 环境。

包含一个或多个 '.' 字符的标识符（因此包含多个标识符成分）被称为 分层标识符。 分层标识符同时用于表示导入名和命名空间中的名称。

5.3. 结构🔗

语法源文件
Parser for a Lean module. We never actually run this parser but instead use the imperative definitions in the parent module that
return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
for it in order to auto-generate helpers such as the pretty printer. module ::=
    Parser for a Lean module. We never actually run this parser but instead use the imperative definitions in the parent module that
return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
for it in order to auto-generate helpers such as the pretty printer. header command*

源文件由一个 文件头，后面跟随一系列 命令 组成。

如果源文件的文件头以 Lean.Parser.Module.headermodule 开头，那么该源文件称为一个 模块。 模块可以更精细地控制向使用方公开哪些信息。

5.3.1. 文件头🔗

文件头列出在当前源文件之前需要精译的源文件。 这些源文件中的声明在当前源文件中可见。

语法文件头

文件头由一个可选的 Lean.Parser.Module.headermodule 关键字和一系列 import 语句组成：

header ::=
    module?
    import*

可选的 prelude 关键字只应在 Lean 源码中出现：

header ::= ...
    | module?
      prelude
      import*

如果存在 prelude 关键字，则表示该文件属于 Lean 前导库 的实现部分，也就是无需任何显式导入即可使用的代码——不应在 Lean 实现之外使用。

语法前导库模块
prelude ::=
    prelude
语法导入

所有源文件都可以使用普通导入：

import ::= ...
    | import ident

对于不是模块的源文件，该语法导入指定的 Lean 文件。 导入文件会让它及其递归导入的所有源文件的内容在当前源文件中可见。

源文件名与命名空间不一定一一对应。 源文件可以向任意命名空间添加名称，而导入源文件不会影响当前打开的命名空间集合。

导入名会通过将名称中的点（.）替换为路径分隔符，并加上 .lean 或 .olean 后缀，转成文件名。 Lean 在其包含路径中搜索对应的中间构建产物或可导入的模块文件。

Modules may use the following import syntax:

import ::= ...
    | public? meta? import all? ident

All imports to a module must themselves be modules. Without modifiers, the imported module's public scope is added to the current module's private scope. The imported module is not made available to modules that import the current module. The modifiers have the following meanings:

public

The imported module's public scope is added to the current module's public scope and made available to the current module's importers.

meta

The contents of the imported module are made available at the meta phase in the current module.

all

The imported module's private scope is added to the current module's private scope.

5.3.2. 命令🔗

命令 是 Lean 的顶级语句。 例如归纳类型声明、定理、函数定义、像 open 或 variable 这样的命名空间修饰符，以及 #check 这样的交互查询，都是命令的例子。 命令的语法是用户可扩展的，而且命令本身还可以 扩展用于解析后续命令的语法。 各类 Lean 命令的详细说明见手册相应章节，下文不再一一枚举。

5.4. Modules and Visibility🔗

A module is a source file that has opted in to a distinction between public and private information. Lean ensures that private information can change without affecting clients that import only its public information. This discipline brings a number of benefits:

Much-improved average build times

Changes to files that affect only non-exported information (e.g. proofs, comments, and docstrings) will not trigger rebuilds outside of these files. Even when dependent files have to be rebuilt, those files that cannot be affected (as determined by their Lean.Parser.Module.importimport annotations) can be skipped.

Control over API evolution

Library authors can trust that changes to non-exported information will not affect downstream users of their library. If only a function's signature is exposed, then downstream users cannot rely on definitional equalities that involve its unfolding; this means that the library's author is free to adopt a more efficient algorithm without unintentionally breaking client code.

Avoiding accidental unfolding

Limiting the scope in which definitions can be unfolded allows for avoiding both reductions that should be replaced by application of more specific theorems as well as unproductive reductions that were not in fact necessary. This improves the speed of proof elaboration.

Smaller executables

Separating compile-time and run-time code allows for more aggressive dead code elimination, guaranteeing that metaprograms such as tactics do not make it into the final binary.

Reduced memory usage

Excluding private information such as proofs from importing can improve Lean's memory use both while building and editing a project. Porting mathlib4 to the module system has shown savings close to 50% from this even before imports are further minimized.

Modules contain two separate scopes: the public scope consists of information that is visible in modules that import a module, while the private scope consists of information that is generally visible only within the module. Some examples of information that can be private or public include:

Names

Constants (such as definitions, inductive types, or constructors) may be private or public. A public constant's type may only refer to public names.

Definitions

A public definition may be exposed or not. If a public definition is not exposed, then it cannot be unfolded in contexts that only have access to the public scope. Instead, clients must rely on the theorems about the definition that are provided in the public scope.

Each declaration has default visibility rules. Generally speaking, all names are private by default, unless defined in a public section. Even public names usually place the bodies of definitions in the private scope, and even proofs in exposed definitions are kept private. The specific visibility rules for each declaration command are documented together with the declaration itself.

Private and Public Definitions

The module Greet.Create defines a function greeting. Because there are no visibility modifiers, this function defaults to the private scope:

Greet/Create.leanmodule def greeting (name : String) : String := s!"Hello, {name}"

The definition of greeting is not visible in the module Greet, even though it imports Greet.Create:

Greet.leanmodule import Greet.Create def greetTwice (name1 name2 : String) : String := Unknown identifier `greeting`greeting name1 ++ "\n" ++ Unknown identifier `greeting`greeting name2 
Unknown identifier `greeting`

If greeting is made public, then greetTwice can refer to it:

Greet/Create.leanmodule public def greeting (name : String) : String := s!"Hello, {name}"
Greet.leanmodule import Greet.Create def greetTwice (name1 name2 : String) : String := greeting name1 ++ "\n" ++ greeting name2
Exposed and Unexposed Definitions

The module Greet.Create defines a public function greeting.

Greet/Create.leanmodule public def greeting (name : String) : String := s!"Hello, {name}"

Although the definition of greeting is visible in the module Greet, it cannot be unfolded in a proof because the definition's body is in the private scope of Greet:

Greet.leanmodule import Greet.Create def greetTwice (name1 name2 : String) : String := greeting name1 ++ "\n" ++ greeting name2 theorem greetTwice_is_greet_twice {name1 name2 : String} : greetTwice name1 name2 = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2 := unsolved goals name1 name2:String⊢ greeting name1 ++ "\n" ++ greeting name2 = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2name1:Stringname2:String⊢ greetTwice name1 name2 = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2 name1:Stringname2:String⊢ greeting name1 ++ "\n" ++ greeting name2 = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2 
Invalid simp theorem `greeting`: Expected a definition with an exposed body

Adding the @[expose] attribute exposes the definition so that downstream modules can unfold greeting:

Greet/Create.leanmodule @[expose] public def greeting (name : String) : String := s!"Hello, {name}"

Now, the proof can proceed:

Greet.leanmodule import Greet.Create def greetTwice (name1 name2 : String) : String := greeting name1 ++ "\n" ++ greeting name2 theorem greetTwice_is_greet_twice {name1 name2 : String} : greetTwice name1 name2 = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2 := name1:Stringname2:String⊢ greetTwice name1 name2 = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2 name1:Stringname2:String⊢ "Hello, " ++ name1 ++ "\n" ++ ("Hello, " ++ name2) = "Hello, " ++ name1 ++ "\n" ++ "Hello, " ++ name2 All goals completed! 🐙
Proofs are Private

In this module, the function incr is public, but its implementation is not exposed:

Main.leanmodule public def incr : Nat → Nat | 0 => 1 | n + 1 => incr n + 1 public theorem incr_eq_plus1 : incr = (· + 1) := ⊢ incr = fun x => x + 1 n:Nat⊢ incr n = n + 1 ⊢ incr 0 = 0 + 1n✝:Nata✝:incr n✝ = n✝ + 1⊢ incr (n✝ + 1) = n✝ + 1 + 1 ⊢ incr 0 = 0 + 1n✝:Nata✝:incr n✝ = n✝ + 1⊢ incr (n✝ + 1) = n✝ + 1 + 1 All goals completed! 🐙

Nonetheless, the proof of the theorem incr_eq_plus1 can unfold its definition. This is because proofs of theorems are in the private scope. This is the case both for public and private theorems.

The option backward.privateInPublic can be used while transitioning from ordinary source files to modules. When it is set to true, private definitions are exported, though their names are not accessible in importing modules. However, references to them in the public part of their defining module are allowed. Such references result in a warning unless the option backward.privateInPublic.warn is set to false. These warnings can be used to locate and eventually eliminate these references, allowing backward.privateInPublic to be disabled. Similarly, backward.proofsInPublic causes proofs created with Lean.Parser.Term.byby to be public, rather than private; this can enable Lean.Parser.Term.byby to fill in metavariables in its expected type. Most use cases for backward.proofsInPublic also require that backward.privateInPublic is enabled.

🔗option
backward.privateInPublic

Default value: false

(module system) Export private declarations, allowing for arbitrary access to them while code is being ported to the module system. Such accesses will generate warnings unless backward.privateInPublic.warn is disabled.

🔗option
backward.privateInPublic.warn

Default value: true

(module system) Warn on accesses to private declarations that are allowed only by backward.privateInPublic being enabled.

🔗option
backward.proofsInPublic

Default value: false

(module system) Do not abstract proofs used in the public scope into auxiliary theorems. Enabling this option may lead to failures or, when backward.privateInPublic and its warn sub-option are enabled, additional warnings from private accesses.

Exporting Private Definitions

In the module L.Defs, the public definition of f refers to the private definition drop2 in its signature. Because backward.privateInPublic is true, this is allowed, resulting in a warning:

L/Defs.leanmodule set_option backward.privateInPublic true def drop2 (xs : List α) : List α := xs.drop 2 public def f (xs : List α) (transform : List α → List α:= Private declaration `drop2` accessed publicly; this is allowed only because the `backward.privateInPublic` option is enabled. Disable `backward.privateInPublic.warn` to silence this warning.drop2) : List α := transform xs 
Private declaration `drop2` accessed publicly; this is allowed only because the `backward.privateInPublic` option is enabled. 

Disable `backward.privateInPublic.warn` to silence this warning.

When the module is imported, references to f use drop2 as a default argument value; however, its name is inaccessible in the module L:

L.leanmodule import L.Defs def xs := [1, 2, 3] set_option pp.explicit true in @f Nat xs (@drop2✝ Nat) : List Nat#check f xs 
@f Nat xs (@drop2✝ Nat) : List Nat
Proofs in Public

In the plain source file NotMod, the definition of two uses the content of the proof to fill out the numeric value in the definition by solving a metavariable:

NotMod.leanstructure Half (n : Nat) where val : Nat ok : val + val = n abbrev two := Half.mk _ <| ⊢ ?m.3 + ?m.3 = ?m.5 ⊢ 2 + 2 = 4 All goals completed! 🐙

Converting this file to a module results in an error, because the body of the definition is exposed in the public part but the proof is private and thus cannot change the public type:

Mod.leanmodule public section structure Half (n : Nat) where val : Nat ok : val + val = n abbrev two := Half.mk _ <| tactic execution is stuck, goal contains metavariables ?m.3 + ?m.3 = ?m.5by show 2 + 2 = 4 rfl 
tactic execution is stuck, goal contains metavariables
  ?m.3 + ?m.3 = ?m.5

Setting the option backward.proofsInPublic causes the proof to be in the public part of the module so it can solve the metavariable:

Mod.leanmodule public section structure Half (n : Nat) where val : Nat ok : val + val = n set_option backward.proofsInPublic true in abbrev two := Half.mk _ <| ⊢ ?m.3 + ?m.3 = ?m.5 ⊢ 2 + 2 = 4 All goals completed! 🐙

However, it is typically better style to reformulate the definition so that the proof has a complete goal:

Mod.leanmodule public section structure Half (n : Nat) where val : Nat ok : val + val = n abbrev two : Half 4 := Half.mk 2 <| ⊢ 2 + 2 = 4 All goals completed! 🐙

The private scope of a module may be imported into another module using the Lean.Parser.Module.importall modifier. By default, this is only allowed if the imported module and the current module are from the same Lake package, as its main purpose is to allow for separating definitions and proofs into separate modules for internal organization of a library. The Lake package or library option allowImportAll can be set to allow other packages to access to the current package's private scopes via Lean.Parser.Module.importimport all. The imported private scope includes private imports of the imported module, including nested Lean.Parser.Module.importimport alls. As a consequence, the set of private scopes accessible to the current module is the transitive closure of Lean.Parser.Module.importimport all declarations.

The module system's Lean.Parser.Module.importimport all is more powerful than Lean.Parser.Module.importimport without the module system. It makes imported private definitions accessible directly by name, as if they were defined in the current module. A secondary use case for Lean.Parser.Module.importimport all is to access code in multiple modules within a library that should nonetheless not be provided to downstream consumers, as well as to allow tests to access information that is not part of the public API.

Importing Private Information

This library separates a module of definitions from a module of lemmas. This is a common pattern in Lean code.

Tree/Basic.leanmodule public inductive Tree (α : Type u) : Type u where | leaf | branch (left : Tree α) (val : α) (right : Tree α) public def Tree.count : Tree α → Nat | .leaf => 0 | .branch left _ right => left.count + 1 + right.count

However, because Tree.count is not exposed, the proof in the lemma file cannot unfold it:

Tree/Lemmas.leanmodule public import Tree.Basic theorem Tree.count_leaf_eq_zero : count (.leaf : Tree α) = 0 := α:Type u_1⊢ leaf.count = 0 `simp` made no progressα:Type u_1⊢ leaf.count = 0 
Invalid simp theorem `count`: Expected a definition with an exposed body

Importing the private scope from Tree.Basic into the lemma module allows the definition to be unfolded in the proof.

Tree/Basic.leanmodule public inductive Tree (α : Type u) : Type u where | leaf | branch (left : Tree α) (val : α) (right : Tree α) public def Tree.count : Tree α → Nat | .leaf => 0 | .branch left _ right => left.count + 1 + right.count
Tree/Lemmas.leanmodule import all Tree.Basic public import Tree.Basic theorem Tree.count_leaf_eq_zero : count (.leaf : Tree α) = 0 := α:Type u_1⊢ leaf.count = 0 All goals completed! 🐙

5.4.1. The Meta Phase🔗

Definitions in Lean result in both a representation in the type theory that is designed for formal reasoning and a compiled representation that is designed for execution. This compiled representation is used to generate machine code, but it can also be executed directly using an interpreter. The code that runs during elaboration, such as tactics or macros, is the compiled form of definitions. If this compiled representation changes, then any code created by it may no longer be up to date, and it must be re-run. Because the compiler performs non-trivial optimizations, changes to any definition in the transitive dependency chain of a function could in principle invalidate its compiled representation. This means that metaprograms exported by modules induce a much stronger coupling than ordinary definitions. Furthermore, metaprograms run during the construction of ordinary terms; thus, they must be fully defined and compiled before use. After all, a function definition without a body cannot be run. The time at which metaprograms are run is referred to as the metaprogramming phase, frequently just called the meta phase.

Just as they distinguish between public and private information, modules additionally distinguish code that is available in the meta phase from ordinary code. Any declaration used as an entry point to compile-time execution has to be tagged with the Lean.Parser.Module.importmeta modifier, which indicates that the declaration is available for use as a metaprogram. This is automatically done in built-in metaprogramming syntax such as Lean.Parser.Command.syntax : commandsyntax, Lean.Parser.Command.macro : commandmacro, and Lean.Parser.Command.elab : commandelab but may need to be done explicitly when manually applying metaprogramming attributes such as app_delab or when defining helper declarations. A Parser.Command.declModifiersmeta definition may only access (and thus invoke) other Parser.Command.declModifiersmeta definitions in execution-relevant positions; a non-Parser.Command.declModifiersmeta definition likewise may only access other non-Parser.Command.declModifiersmeta definitions.

Meta Definitions

In this module, the helper function revArrays reverses the order of the elements in each array literal in a term. This is called by the macro rev!.

Main.leanmodule open Lean variable [Monad m] [MonadRef m] [MonadQuotation m] partial def revArrays : Syntax → m Term | `(#[$xs,*]) => `(#[$((xs : Array Term).reverse),*]) | other => do match other with | .node k i args => pure ⟨.node k i (← args.mapM revArrays)⟩ | _ => pure ⟨other⟩ Invalid `meta` definition `_aux___macroRules_termRev!__1`, `revArrays` not marked `meta`macro "rev!" e:term : term => do revArrays e

The error message indicates that revArrays cannot be used from the macro because it is not defined in the module's metaprogramming phase:

Invalid `meta` definition `_aux___macroRules_termRev!__1`, `revArrays` not marked `meta`

Marking revArrays with the Lean.Parser.Command.declModifiers`declModifiers` 是声明修饰符的集合，包括： * 文档注释 `/-- ... -/` * 属性列表 `@[attr1, attr2]` * 可见性说明符 `private` 或 `public` * `protected` * `noncomputable` * `unsafe` * `partial` 或 `nonrec` 所有修饰符都是可选的，并且必须按上述顺序出现。 `nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。meta modifier allows the macro definition to call it:

Main.leanmodule open Lean variable [Monad m] [MonadRef m] [MonadQuotation m] meta partial def revArrays : Syntax → m Term | `(#[$xs,*]) => `(#[$((xs : Array Term).reverse),*]) | other => do match other with | .node k i args => pure ⟨.node k i (← args.mapM revArrays)⟩ | _ => pure ⟨other⟩ macro "rev!" e:term : term => do revArrays e #[3, 2, 1]#eval rev! #[1, 2, 3] 
#[3, 2, 1]

Libraries that were not originally part of the meta phase can be brought into it by importing a module with Parser.Module.importmeta import. When a module is imported at the meta phase, all of its definitions are made available at that phase, whether or not they were marked Parser.Command.declModifiersmeta. There is no meta-meta phase. In addition to making the imported module's public contents available at the meta phase, Parser.Module.importmeta import indicates that the current module should be rebuilt if the compiled representation of the imported module changes, ensuring that modified metaprograms are re-run. If a definition should be usable in both phases, then it must be defined in a separate module and imported at both phases.

Cross-Phase Code Reuse

In this module, the function toPalindrome is defined in the meta phase, which allows it to be used in a macro but not in an ordinary definition:

Phases.leanmodule open Lean variable [Monad m] [MonadRef m] [MonadQuotation m] meta def toPalindrome (xs : Array α) : Array α := xs ++ xs.reverse meta partial def palArrays : Syntax → m Term | `(#[$xs,*]) => `(#[$(toPalindrome (xs : Array Term)),*]) | other => do match other with | .node k i args => pure ⟨.node k i (← args.mapM palArrays)⟩ | _ => pure ⟨other⟩ macro "pal!" e:term : term => do palArrays e #[1, 2, 3, 3, 2, 1] ++ [6, 7, 8] : Array Nat#check pal! (#[1, 2, 3] ++ [6, 7, 8]) public def Invalid definition `colors`, may not access declaration `toPalindrome` marked as `meta`colors := toPalindrome #["red", "green", "blue"] 
Invalid definition `colors`, may not access declaration `toPalindrome` marked as `meta`

Moving toPalindrome to its own module, Phases.Pal, allows this module to be imported at both phases:

Phases/Pal.leanmodule public def toPalindrome (xs : Array α) : Array α := xs ++ xs.reverse
Phases.leanmodule meta import Phases.Pal import Phases.Pal open Lean variable [Monad m] [MonadRef m] [MonadQuotation m] meta partial def palArrays : Syntax → m Term | `(#[$xs,*]) => `(#[$(toPalindrome (xs : Array Term)),*]) | other => do match other with | .node k i args => pure ⟨.node k i (← args.mapM palArrays)⟩ | _ => pure ⟨other⟩ local macro "pal!" e:term : term => do palArrays e #[1, 2, 3, 3, 2, 1] ++ [6, 7, 8] : Array Nat#check pal! (#[1, 2, 3] ++ [6, 7, 8]) public def colors := toPalindrome #["red", "green", "blue"]

If the macro pal! were public (that is, if it was not declared with the local modifier) then the Lean.Parser.Module.importmeta import of Phases.Pal would need to be declared Lean.Parser.Module.importpublic as well.

In addition, the import must be public if the imported definition may be executed at compile time outside the current module, i.e. if it is reachable from some public Parser.Command.declModifiersmeta definition in the current module. Use Parser.Module.importpublic meta import. If the declaration is already declared Parser.Command.declModifiersmeta, then Parser.Module.importpublic import is sufficient.

Unlike definitions, most metaprograms are public by default. Thus, most Lean.Parser.Module.importmeta import are also Parser.Module.importpublic in practice. The exception is when a definition is imported solely for use in local metaprograms, such as those declared with Parser.Command.syntaxlocal syntax, Parser.Command.macrolocal macro, or Parser.Command.elablocal elab.

As a guideline, it is usually preferable to keep the amount of Lean.Parser.Command.declModifiers`declModifiers` 是声明修饰符的集合，包括： * 文档注释 `/-- ... -/` * 属性列表 `@[attr1, attr2]` * 可见性说明符 `private` 或 `public` * `protected` * `noncomputable` * `unsafe` * `partial` 或 `nonrec` 所有修饰符都是可选的，并且必须按上述顺序出现。 `nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。meta annotations as small as possible. This avoids locking otherwise-reusable declarations into the meta phase and it helps the build system avoid more rebuilds. Thus, when a metaprogram depends on other code that does not itself need to be marked Lean.Parser.Command.declModifiers`declModifiers` 是声明修饰符的集合，包括： * 文档注释 `/-- ... -/` * 属性列表 `@[attr1, attr2]` * 可见性说明符 `private` 或 `public` * `protected` * `noncomputable` * `unsafe` * `partial` 或 `nonrec` 所有修饰符都是可选的，并且必须按上述顺序出现。 `nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。meta, this other code should be placed in a separate module and not marked Lean.Parser.Command.declModifiers`declModifiers` 是声明修饰符的集合，包括： * 文档注释 `/-- ... -/` * 属性列表 `@[attr1, attr2]` * 可见性说明符 `private` 或 `public` * `protected` * `noncomputable` * `unsafe` * `partial` 或 `nonrec` 所有修饰符都是可选的，并且必须按上述顺序出现。 `nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。meta. Only the final module that actually registers a metaprogram needs the helpers to be in the meta phase. This module should use Lean.Parser.Module.importpublic meta import to import those helpers and then define its metaprograms using built-in syntax like Parser.Command.elabelab, using Lean.Parser.Command.declaration : commandmeta def, or using Lean.Parser.Command.section : commandA `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local` commands. Sections can be nested. `section <id>` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file. meta section.

5.5. 精译后的模块🔗

Lean 在精译一个源文件时，最终会得到一个 环境。 该环境包括本文件声明的常量、归纳类型、定理、类型类、实例及其它所有声明，还有用于记录各种数据（如 simp 集、命名空间别名、文档注释）的辅助表。 如果文件包含模块，环境还会记录哪些信息是公开或私有的，以及定义在哪个阶段可用。

Lean 处理源文件时，命令会不断向环境中添加内容。 精译完成后，环境会被序列化为一个 .olean 文件，其中既包含环境，也包含环境所需运行时对象的压缩堆区。 这意味着被导入的源文件无需重新执行所有命令即可加载。 精译模块所得的环境会被序列化为三个 .olean 文件，分别保存环境中的私有信息、公开信息和服务器信息。 服务器信息包括 API 文档和定义的源码位置等数据；它们只在使用 Lean 语言服务器时需要，无需随公开信息一起加载。

5.6. Module System Errors and Patterns🔗

The following list contains common errors one might encounter when using the module system and especially porting existing files to the module system:

Unknown constant errors

Check whether a private definition is being accessed in the public scope. If so, the problem can be solved by making the current declaration private as well, or by placing the reference into the private scope using the Lean.Parser.Term.structInstFieldDef : structInstFieldDeclprivate modifier on a field or Lean.Parser.Term.byby for a proof.

Definitional equality errors, especially after porting

Failures of expected definitional equalities are usually due to a missing expose attribute on a definition or alternatively, if imported, an Lean.Parser.Module.importimport all. Prefer the former if anyone outside your library might feasibly require the same access. The error message should list non-exposed definitions that could not be unfolded. This may also appear as a kernel error when a tactic directly emits proof terms that reference specific declarations without going through the elaborator, such as for proof by reflection. In this case, there is no readily available trace for debugging; consider using @[expose]‍ Parser.Command.sectionsections generously on the closure of relevant modules.

5.6.1. Recipe for Porting Existing Files🔗

To gain the benefits of the module system, source files must be made into modules. Start by enabling the module system throughout all files with minimal breaking changes:

  1. Prefix all files with Lean.Parser.Module.headermodule.

  2. Make all existing imports Lean.Parser.Command.declModifiers`declModifiers` 是声明修饰符的集合，包括： * 文档注释 `/-- ... -/` * 属性列表 `@[attr1, attr2]` * 可见性说明符 `private` 或 `public` * `protected` * `noncomputable` * `unsafe` * `partial` 或 `nonrec` 所有修饰符都是可选的，并且必须按上述顺序出现。 `nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。public unless they will be used only in proofs.

  • Add Lean.Parser.Module.importimport all when errors that mention references to private data occur.

  • Add Lean.Parser.Module.importpublic meta import when errors that mention “must be Lean.Parser.Module.importmeta” occur. The Lean.Parser.Module.importpublic may be omitted when defining local-only metaprograms.

  1. Prefix the remainder of the file with @[expose] public section or, for programming-focused files, with Lean.Parser.Command.section : commandA `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local` commands. Sections can be nested. `section <id>` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file. public section. The latter should be used for programs that will be run but not reasoned about.

After an initial build under the module system succeeds, the dependencies between modules can be iteratively minimized. In particular, removing uses of Lean.Parser.Command.declModifiers`declModifiers` 是声明修饰符的集合，包括： * 文档注释 `/-- ... -/` * 属性列表 `@[attr1, attr2]` * 可见性说明符 `private` 或 `public` * `protected` * `noncomputable` * `unsafe` * `partial` 或 `nonrec` 所有修饰符都是可选的，并且必须按上述顺序出现。 `nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。public and @[expose] will help avoid unnecessary rebuilds.

5.7. 包、库与目标🔗

Lean 模块被组织为 包，包是代码分发的单位。 一个 包 可以包含多个库或可执行文件。

包中面向其他 Lean 包复用的代码会被组织为 库。 面向编译并作为独立程序运行的代码被组织为 可执行文件。 包、库、可执行文件将在 Lake，Lean 标准构建工具 一节中详细介绍。